\documentclass{llncs}

\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}

\usepackage{macros}


\pagestyle{plain}

\begin{document}

\begin{figure}[t]
\input{proof-system}
\caption{ Matching logic proof system}
\label{fig:proof-system}
\vspace*{-2ex}
\end{figure}

Fig.~\ref{fig:proof-system} shows our nine-rule proof system for deriving
matching logic reduction rules.  Initially, $\cal A$ contains the operational
semantics of the target language.  The first group of rules (Reflexivity, Axiom,
Substitution, Transitivity) have an operational nature and are needed to execute
reduction systems; any executable semantic framework is expected to have similar
rules (see, e.g., rewriting logic~\cite{meseguer92}).  The second group of rules
(Case Analysis, Logic Framing, Consequence and Abstraction) have a deductive
nature and are inspired from the subset of language-independent rules of Hoare
logic~\cite{hoare-69}.

The Circularity proof rule is new.  It {\em language-independently} captures the
various circular behaviors that appear in languages, due to loops, recursion,
jumps, etc.
%
\begin{definition}
\label{dfn:Raplus}

Let $\LongRap{\cal A}{\varphi}{\varphi'}$ be the derivation relation obtained by
dropping the Reflexivity rule from the proof system in Fig.~\ref{fig:proof-system}.

\end{definition}
%
The intuition for $\LongRap{\cal A}{\varphi}{\varphi'}$ is that a configuration
satisfying $\varphi$ needs at least one operational semantics step to transit to
one satisfying $\varphi'$.  The Circularity rule in Fig.~\ref{fig:proof-system}
says that we can derive the sequent $\LongRa{\cal A}{\varphi}{\varphi'}$
whenever we can derive the rule $\varphi \Ra \varphi'$ by starting with one or
more reduction steps in ${\cal A}$ and continuing with steps which can involve
both rules from ${\cal A}$ and the rule to be proved itself, $\varphi \Ra
\varphi'$.  The first step can for example be a loop unrolling step in the case
of loops, or a function invocation step in the case of recursive functions, etc.
%
The use of the claimed properties in their own proofs in Circularity is
reminiscent of {\em circular coinduction} \cite{rosu-lucanu-2009-calco}.  Like
in circular coinduction, where the claimed properties can only be used in some
special contexts, Circularity also disallows their unrestricted use: it only
allows them to be guarded by a trusted, operational step.  It would actually be
unsound to drop the operational-step-guard requirement: for example, if ${\cal
A}$ contained $\varphi_1 \Ra \varphi_2$ then $\varphi_2 \Ra \varphi_1$ could be
``proved'' in a two-step transitivity, using itself, the rule in $\cal A$ and
then itself again.

\begin{theorem}
%
\label{thm:partial-correctness}
%
\textbf{(partial correctness)} Let $\cal S$ be a well-defined and deterministic
matching logic reduction system (typically corresponding to an operational
semantics), and let $\LongRa{\cal S}{\varphi}{\varphi'}$ be a sequent derived
with the proof system in Fig.~\ref{fig:proof-system}.  Then ${\cal S} \models
\varphi \Ra \varphi'$ (see Appendix~\ref{sec:proofs} for the proof).
%
\end{theorem}

Hence, proof derivations with the system in Fig.~\ref{fig:proof-system} are
sound w.r.t.\ the (transition system generated by the) operational semantics, in
the sense of partial correctness.  The well-definedness requirement is
acceptable (operational semantics satisfy it) and needed (otherwise not even the
axioms satisfy ${\cal S} \models \varphi \Ra \varphi'$).  The determinism
requirement is {\em unnecessary} in the proof of Theorem
\ref{thm:partial-correctness}, but it makes the result mean partial correctness.
Without it, ${\cal S} \models \varphi \Ra \varphi'$ (see
Definition~\ref{def:partial-correctness}) means ``any terminating configuration
that matches $\varphi$ reduces, on some possible execution path, to a
configuration that matches $\varphi'$''.  Determinism enforces ``some path'' to
be equal to ``all paths''.

We illustrate our proof system by means of some examples.  The proof below may
seem low level when compared to the similar proof done using Hoare logic.
However, note that it is quite mechanical, the user only having to provide the
invariant ($\varphi_{\rm inv}$).  The rest is automatic and consists of applying
the operational reduction rules whenever they match, except for the
circularities which are given priority; when the redex is an {\tt if}, a Case
Analysis is applied.  Our current MatchC implementation can prove it
automatically, as well as much more complex programs (see
Section~\ref{sec:implementation}).  Although the paper Hoare logic proofs for
simple languages like IMP may look more compact, note that in general they make
assumptions which need to be addressed in implementations, such as that
expressions do not have side effects, or that substitution is available and
atomic, etc.

Consider the \texttt{SUM} code (Section~\ref{sec:matching-logic-reduction}) 
%
``{\verb|s:=0; while(n>0)(s:=s+n; n:=n-1)|}'',
%
and the next property given as a matching logic reduction rule, say $\mu_{\tt
SUM}^1 \equiv (\varphi_\LHS \Rightarrow \varphi_\RHS)$:
%
$$
%
\cfg{\texttt{SUM}}{(\texttt{s}\mapsto s,\ \texttt{n}\mapsto n)} \wedge n
\geq_{\it Int} 0 \Ra \cfg{\texttt{skip}}{(\texttt{s}\mapsto n*_{\it Int}(n+_{\it
Int}1)/_{\it Int}2,\ \texttt{n}\mapsto 0)}
%
$$
%
Let us formally derive this property using the proof system in
Fig.~\ref{fig:proof-system}. Let ${\cal S}$ be the operational semantics of
\IMP{} in Fig.~\ref{fig:IMP} and let $\varphi_{\rm inv}$ be the pattern
%
$$
%
\cfg{{\tt LOOP}}{(\texttt{s} \mapsto (n -_\Int n')*_\Int(n +_\Int n' +_\Int
1)/_\Int 2,\ {\tt n} \mapsto n')} \ \andx \ n' \geq_\Int 0
%
$$
%
where ${\tt LOOP}$ is 
%
``{\verb|while (n>0) (s := s+n; n := n-1)|}''.
%
We derive ${\cal S} \vdash \mu_{\tt SUM}^1$ by Transitivity with $\mu_1 \equiv
(\varphi_\LHS \Ra \exists n' \varphi_{\rm inv})$ and $\mu_2 \equiv (\exists n'
\varphi_{\rm inv} \Ra \varphi_\RHS)$.  By Axiom {\bf asgn} (Fig.~\ref{fig:IMP},
within the \texttt{SUM} context) followed by Substitution with $\theta(\sigma) =
({\tt s} \mapsto s,\ {\tt n} \mapsto n)$, $\theta(x) = {\tt s}$ and $\theta(i) =
0$ followed by Logic Framing with $n \geq_\Int 0$, we derive $\varphi_\LHS \Ra
\cfg{{\tt skip; LOOP}}{({\tt s} \mapsto 0,\ {\tt n} \mapsto n)} \mathrel{\andx}
n \geq_\Int 0$.  This ``operational'' sequence of \underline{A}xiom,
\underline{S}ubstitution and \underline{L}ogic \underline{F}raming is quite
common; we abbreviate it ASLF.  Further, by ASLF with ${\bf seq}$ and
Transitivity, we derive $\varphi_\LHS \Ra \cfg{{\tt LOOP}}{({\tt s} \mapsto s, \
{\tt n} \mapsto n)} \mathrel{\andx} n \geq_{\it Int} 0$.  ${\cal S} \vdash
\mu_1$ now follows by Consequence.
%
We derive ${\cal S} \vdash \mu_2$ by Circularity with ${\cal S} \vdash \exists
n' \varphi_{\rm inv} \Ra^+ \varphi_{\tt if}$ and ${\cal S} \cup \{ \mu_2 \}
\vdash \varphi_{\tt if} \Ra \varphi_\RHS$, where $\varphi_{\tt if}$ is the
formula obtained from $\varphi_{\rm inv}$ replacing its code with
%
``{\verb|if (n>0) (s := s+n; n := n-1; LOOP) else skip|}''.
%
ASLF (${\bf while}$) followed by Abstraction derive ${\cal S} \vdash \exists n'
\varphi_{\rm inv} \Ra^+ \varphi_{\tt if}$.  For the other, we use Case Analysis
with $\varphi_{\tt if} \wedge n' \leq_{\it Int} 0$ and $\varphi_{\tt if} \wedge
n' >_{\it Int} 0$.  ASLF ({\bf lookup}$_{\tt n}$, {\bf op}$_{\tt >}$, {\bf
cond}$_2$) together with some Transitivity and Consequence steps derive ${\cal
S} \cup \{ \mu_2 \} \vdash \varphi_{\tt if} \wedge n' \leq_{\it Int} 0 \Ra
\varphi_\RHS$ ($\mu_2$ is not needed in this derivation).  Similarly, ASLF ({\bf
lookup}$_{\tt n}$, {\bf op}$_{\tt >}$, {\bf cond}$_1$, {\bf lookup}$_{\tt n}$,
{\bf lookup}$_{\tt s}$, {\bf op}$_{\tt +}$, {\bf asgn}, {\bf seq}, {\bf
lookup}$_{\tt n}$, {\bf op}$_{\tt -}$, {\bf asgn}, {\bf seq}, and $\mu_2$)
together with Transitivity and Consequence steps derive ${\cal S} \cup \{ \mu_2
\} \vdash \varphi_{\tt if} \wedge n' >_{\it Int} 0 \Ra \varphi_\RHS$.  This time
$\mu_2$ is needed and it is interesting to note how.  After applying all the
steps above and the \texttt{LOOP} fragment of code is reached again, the pattern
characterizing the configuration is
%
$$
%
\cfg{{\tt LOOP}}{(\texttt{s} \mapsto (n -_\Int n')*_\Int(n +_\Int n' +_\Int
1)/_\Int 2 \mathrel{+_\Int} n',\ {\tt n} \mapsto n'-_\Int1)} \ \andx \ n' >_\Int
0
%
$$
%
The circularity $\mu_2$ can now be applied, via Consequence and Transitivity,
because this formula implies $\exists n' \varphi_{\rm inv}$ (indeed, pick the
existentially quantified $n'$ to be $n' -_\Int 1$).

We can similarly derive the other reduction rule for \texttt{SUM} in
Section~\ref{sec:matching-logic-reduction}, say $\mu_{\tt SUM}^2$.  Instead, let
us prove the stronger result that the two matching logic reduction rules are
equivalent, that is, that ${\mu_{\tt SUM}^1} \mathrel\vdash \mu_{\tt SUM}^2$ and
${\mu_{\tt SUM}^2} \mathrel\vdash \mu_{\tt SUM}^1$.  Using conventional FOL
reasoning and the Consequence proof rule, one can show $\mu_{\tt SUM}^2$
equivalent to the reduction rule
%
$$ \exists s\ (\cfg{\texttt{SUM}}{\!\!(\texttt{s}\!\mapsto\!\! s,
\texttt{n}\!\mapsto\! {\it oldn})} \wedge{\it oldn}\!\geq_\Int\!\! 0) \Ra
\cfg{\texttt{skip}}{\!(\texttt{s}\!\mapsto\! \textit{oldn}\!*_{\it
Int}\!(\textit{oldn}\!+_{\it Int}\!1)/_{\it Int}2, \texttt{n}\!\mapsto\! 0)} $$
%
The equivalence to $\mu_{\tt SUM}^1$ now follows by applying the Substitution
rule with $\textit{oldn} \mapsto n$ and Consequence, and, respectively,
Substitution with $n \mapsto \textit{oldn}$ and Abstraction.

Following an approach similar to that in \cite{rosu-ellison-schulte-2010-amast},
we can show that, in the case of IMP, any property derived using its Hoare logic
proof system can also be derived using our proof system in
Fig.~\ref{sec:proof-system}, of course modulo the representation of Hoare
triples as matching logic reduction rules described in
Section~\ref{sec:matching-logic-reduction}.  For example, a Hoare logic proof
step for \texttt{while} is translated in our proof system into an Axiom step
(with \textbf{while} in Fig.~\ref{fig:IMP}), a Case Analysis (for the resulting
\texttt{if} statement), a Circularity (as part of the positive case, when the
\texttt{while} statement is reached again), an Abstraction (to add existential
quantifiers for the logical variables added as part of the translation), and a
few Transitivity steps.  Thus, one can argue that for the particular case of the
IMP language, our proof system in Fig.~\ref{fig:proof-system} is relatively
complete.  We believe that one can prove a generic relative completeness result
for matching logic reduction, but that is beyond the scope of this paper.


\section{Implementation in MatchC}
\label{sec:implementation}

The main concern to a verification framework based on operational semantics is
that it may not be practical, due to the amount of required user involvement or
to the amount of low-level details that needs to be provided in specifications.
%
To test the practical effectiveness of matching logic reduction, we picked a
fragment of C, called KernelC, and implemented a proof-of-concept program
verifier for it based on matching logic, named MatchC. KernelC is quite
expressive, including functions, structures, pointers and I/O primitives.
MatchC uses matching logic reduction rules for program specifications and its
implementation is directly based on the proof system in
Fig.~\ref{fig:proof-system}. It uses the operational semantics of KernelC {\em
completely unchanged} for program verification.

MatchC has verified various programs manipulating lists and trees, performing
arithmetic and I/O operations, and implementing sorting algorithms, binary
search trees, AVL trees, and the Schorr-Waite graph marking algorithm.  In all
these, the users only provide the program specifications, as matching logic
reduction rules but using a user-friendly annotation-based interface, in
addition to the unavoidable formalizations of the mathematical domains of
interest.  The rest is automatic.  For example, it takes MatchC less than 2
seconds to verify Schorr-Waite for full correctness.  The Matching Logic web
page, \url{http://fsl.cs.uiuc.edu/ml}, contains an online interface to run
MatchC, where users can try more than 50 existing examples (or type their own).

Let ${\cal S}$ be the reduction system giving the semantics of KernelC, and let
${\cal C}$ be the set of reduction rules corresponding to user-provided
specifications (properties that one wants to verify).
%
MatchC derives the rules in ${\cal C}$ using the proof system in
Fig.~\ref{fig:proof-system}.  It begins by applying Circularity for each rule in
${\cal C}$ and reduces the task to deriving sequents of the form $\LongRa{{\cal
S} \cup {\cal C}}{\varphi}{\varphi'}$.
%
To prove them, it reduces $\varphi$ iteratively using the rules in ${\cal S}
\cup {\cal C}$ searching for a formula that implies $\varphi'$.  An SMT solver
(Z3~\cite{DBLP:conf/tacas/MouraB08}) is invoked to solve the side conditions of
the rules.  Whenever the reduction rule for a conditional statement cannot apply
because its condition is symbolic, a Case Analysis is applied and formula split
into a disjunction.  Rules in $\cal C$ are given priority; thus, if each loop
and function is given a specification then MatchC will always terminate (Z3
cutoff is 5s).

A previous version of MatchC, based on the proof system
in~\cite{rosu-ellison-schulte-2010-amast}, was discussed
in~\cite{rosu-stefanescu-2011-nier-icse}.  The new implementation based on the
proof system in Fig.~\ref{fig:proof-system} will be presented in detail
elsewhere.  We here only mean to highlight the practical feasibility of our
approach.


\section{Conclusion, Additional Related Work, and Future Work}
\label{sec:conclusion}

To our knowledge, the proof system in Fig.~\ref{fig:proof-system} is the first
of its kind.  Its practical benefits may be considerable.  We now only define
{\em one} semantics of the target language, which is operational and thus
well-understood and comparatively easier than defining an axiomatic semantics.
Moreover, the semantics is testable using existing rewrite engines or functional
languages incorporating pattern matching (e.g., Haskell).  For example, we can
test it by executing program benchmarks that compiler testers use.  This has
already been done for C~\cite{ellison-rosu-2012-popl}.  Then, we take this
semantics and use it {\em as is} for program verification.  Not only that we now
completely skip the tedious step of having to prove the relationship between an
operational and an axiomatic semantics of the same language, but we can also
change the language at will (or fix semantic bugs), without having to worry
about doing that in two different places and maintaining the soundness proofs.

The idea of regarding a program as a specification transformer to analyze
programs in a forwards-style goes back to Floyd in
1967~\cite{Floyd:AssignMeaningProg}.  However, unlike ours, Floyd's rules are
language-specific, not executable, and introduce quantifiers.
%
Dynamic logic~\cite{Harel84dynamiclogic,KeYBook2007} extends FOL with modal
operators to embed program fragments within program specifications.  Like in
matching logic, programs and specifications coexits in the same logic.  However,
unlike in our approach, one still needs to define an alternative (dynamic logic)
semantics of the language, with language-specific proof rules, as one cannot use
a conventional operational semantics with a language-independent proof system.

We believe our proof system can be extended to work with SOS-style {\em
conditional} reduction rules.  Concurrency and non-determinism were purposely
left out; these are major topics which deserve full attention.  The relationship
to Hoare logic was only sketched; details need to be worked out.  Relative
completeness and total correctness also need to be addressed.  Like other formal
semantics, matching logic can also be embedded into higher-level formalisms and
theorem provers, so that proofs of relationships to other semantics can be
mechanized, and even programs verified and formal proof objects produced.
Ultimately, we would like to have a generic verifier taking an operational
semantics as input, together with extension allowing users to provide pattern
annotations, and to yield an automated program verifier based on the proof
system in Fig.~\ref{fig:proof-system}.


\bibliographystyle{splncs03}
\bibliography{refs}


\include{rosu-stefanescu-2012-tr-appendix}


\end{document}



% \renewcommand{\S}{\ensuremath{\mathcal{S}}}
% \newcommand{\A}{\ensuremath{\mathcal{A}}}
% \newcommand{\T}{\ensuremath{\mathcal{T}}}

% \newcommand{\rewriteonce}{\ensuremath{\mathrel{\Rightarrow}}}
% \newcommand{\rewritestar}{\ensuremath{\mathrel{\Rightarrow^*}}}
% \newcommand{\rewriteplus}{\ensuremath{\mathrel{\Rightarrow^+}}}
% \newcommand{\Ansound}{\ensuremath{\mbox{$(\A, n)$-sound}}}

% \newcommand{\svdash}{\ensuremath{\mathrel{\vdash^{2-9}}}}

% \theoremstyle{definition} \newtheorem{definition}{Definition}
% \theoremstyle{plain} \newtheorem{lemma}{Lemma}
% \theoremstyle{plain} \newtheorem{theorem}{Theorem}
% \theoremstyle{plain} \newtheorem{proposition}{Proposition}
% \theoremstyle{plain} \newtheorem{corollary}{Corollary}

% \begin{document}

% Let $\A$ be a matching logic rewrite system and let $n \in
% \mathbb{N}$ be a natural number.

% \begin{definition}

%   We say that a matching logic
%   rewrite rule \mbox{$\varphi \rewriteonce \varphi'$} is
%   \emph{$\Ansound$}
%   (and respectively \emph{\mbox{properly $\Ansound$}}) if for
%   all configurations $\gamma \in \T$ such that
%   $\gamma$ terminates \emph{in at most $n$ steps} in $(\T,
%   \rewriteonce_\A^\T)$ and for all valuations $\rho$ such that
%   $(\gamma, \rho) \models \varphi$, there exists $\gamma'$ such that
%   $\gamma \rewritestar \gamma'$ (respectively $\gamma \rewriteplus
%   \gamma'$) and $(\gamma', \rho) \models \varphi'$.

% \end{definition}

% Note that the difference between ``$\A \models \varphi \rewriteonce
% \varphi'$'' and ``$\varphi \rewriteonce \varphi'$ is $\Ansound$'' is
% \emph{emphasized} in the above definition: we require $\gamma$ to
% terminate in at most $n$ steps. The \emph{proper} version of soundness
% requires that $\gamma$ takes at least one step. For symmetry, we will
% say that $\varphi \rewriteonce \varphi'$ is \mbox{$\A$-sound} if $\A
% \models \varphi \rewriteonce \varphi'$. We immediately have that:

% \begin{proposition}

%   For any matching logic rewrite system $\A$ and any matching logic
%   rewrite rule $\varphi \rewriteonce \varphi'$, \[\A \models \varphi
%   \rewriteonce \varphi'\mbox{ iff for all $n \in \mathbb{N}$, $\varphi
%     \rewriteonce \varphi'$ is $\Ansound$}.\]

% \end{proposition}

% For any two matching logic rewrite systems $\A$ and $\A'$ and any $n
% \in \mathbb{N}$, we will say that $\A'$ is $\Ansound$ (and
% respectively properly $\Ansound$) if for all matching logic rewrite
% rule $\varphi \rewriteonce \varphi' \in \A'$ we have $\varphi
% \rewriteonce \varphi'$ is $\Ansound$ (respectively properly
% $\Ansound$).

% We write $\svdash$ for the deduction relation built from the all the
% inference rules except \textsc{Reflexivity}. Therefore, $\A \svdash
% \varphi \rewriteonce \varphi'$ is equivalent to the notation $\A
% \vdash \varphi \rewriteplus \varphi'$ in the technical report. We use
% our notation to emphasize that we are using a different set of
% inference rules and that $\rewriteplus$ does not refer to the
% transitive closure of $\rewriteonce$.

% \vspace{0.5cm}

% Let $\S$ be a (fixed) matching logic rewrite system. From hereon, we
% will write ``(properly) sound'' instead of ``(properly) $\S$-sound''
% and ``(properly) $n$-sound'' instead of ``(properly) $(\S,
% n)$-sound''. Note that $\S$ itself is trivially properly sound.

% \vspace{0.5cm}

% \begin{lemma}

%   \label{lemma:soundness29}

%   If $P$ is a proof tree (for the $\svdash$ inference relation)
%   concluding $\A \svdash \varphi \rewriteonce \varphi'$ and $\A$ is
%   properly $n$-sound, then $\varphi \rewriteonce \varphi'$ is properly
%   $n$-sound.

% \end{lemma}
% \begin{proof}[Proof sketch]

%   By induction on $P$. If $P$ ends with one of the rules $2-8$, the
%   result is immediate from the induction hypothesis. If $P$ ends with
%   an application of the \textsc{Circularity} rule, we prove by
%   induction on $0 \leq m \leq n$ that $\varphi \rewriteonce \varphi'$
%   is properly $m$-sound:

%   \begin{enumerate}

%   \item if $m = 0$, let $\gamma$ be a normal form (i.e. configuration
%     terminating in at most $0$ steps) w.r.t. $\rewriteonce_\S^\T$ and
%     $\rho$ be a valuation s.t. $(\gamma, \rho) \models \varphi$. As
%     $\A \svdash \varphi \rewriteonce \varphi''$ is the conclusion of a
%     proof tree smaller than $P$, we have by the induction hypothesis
%     and proper $n$-soundness of $\A$ that there exists $\gamma''$ such
%     that $\gamma \rewriteplus \gamma''$ and $(\gamma'', \rho) \models
%     \varphi''$. But $\gamma$ was assumed to be a normal form and
%     therefore this case is impossible.

%   \item if $m > 0$, we assume that $\varphi \rewriteonce \varphi'$ is
%     properly $(m-1)$-sound and we show that $\varphi \rewriteonce
%     \varphi'$ is properly $m$-sound.

%     We have that $\A$ is also properly $(m-1)$-sound (since $m \leq n
%     + 1$ and $\A$ is $n$-sound). Therefore $\A \cup \{\varphi
%     \rewriteonce \varphi'\}$ is $m-1$ sound. By the induction
%     hypothesis, as $\A \cup \{\varphi \rewriteonce \varphi'\} \svdash
%     \varphi" \rewriteonce \varphi'$ is the conclusion of a tree
%     smaller than $P$, we have that $\varphi'' \rewriteonce \varphi'$
%     is $(m-1)$-sound.

%     Let $\gamma$ be an arbitrary configuration which terminates in at
%     most $m$ steps and let $\rho$ be an arbitrary valuation such that
%     $(\gamma, \rho) \models \varphi$. As $\A \svdash \varphi \rewriteonce
%     \varphi''$ is the conclusion of a proof tree smaller than $P$, we
%     have by the induction hypothesis that there exists $\gamma''$ such
%     that $\gamma \rewriteplus_\S^\T \gamma''$ and $(\gamma'', \rho)
%     \models \varphi''$. As $\gamma$ terminates in at most $m$ steps
%     and $\gamma \rewriteplus_\S^\T \gamma''$,
%     we have that $\gamma''$ terminates in at most $m - 1$ steps.
%     As $\varphi'' \rewriteonce \varphi'$ is properly $(m-1)$-sound and
%     $(\gamma'', \rho) \models \varphi''$, we have
%     that there exists $\gamma'$ such that $\gamma'' \rewriteplus_\S^\T
%     \gamma'$ and $(\gamma', \rho) \models \varphi'$. By transitivity,
%     we have $\gamma \rewriteplus_\S^\T \gamma'$. Since $\gamma$ was
%     chosen arbitrarily such that it terminates in at most $m$ steps,
%     we conclude that $\varphi \rewriteonce \varphi'$ is properly
%     $m$-sound.
    
%   \end{enumerate}

%   In particular, for $m = n$, we have obtained exactly what we had to
%   prove: $\varphi \rewriteonce \varphi'$ is properly $n$-sound.

% \end{proof}

% \begin{corollary}

%   \label{corollary:soundness29}

%   If $\A$ is properly sound and $A \svdash \varphi \rewriteonce
%   \varphi'$, then $\varphi \rewriteonce \varphi'$ is properly sound.

% \end{corollary}
% \begin{proof}Immediate from Lemma~\ref{lemma:soundness29}.
% \end{proof}

% \vspace{0.5cm}

% \begin{lemma}
  
%   \label{lemma:soundness19}

%   If $P$ is a proof tree (for the $\vdash$ inference relation)
%   concluding $A \vdash \varphi \rewriteonce \varphi'$ and $\A$ is
%   properly $n$-sound, then $\varphi \rewriteonce \varphi'$ is
%   $n$-sound.

% \end{lemma}
% \begin{proof}

%   Along the lines of Lemma~\ref{lemma:soundness29}~(use
%   Lemma~\ref{lemma:soundness29} for the $2-9$ proof tree in
%   the \textsc{Circularity} rule).

% \end{proof}

% \begin{corollary}

%   \label{corollary:soundness19}

%   If $\A$ is properly sound and $A \vdash \varphi \rewriteonce
%   \varphi'$, then $\varphi \rewriteonce \varphi'$ is sound.

% \end{corollary}
% \begin{proof}
% Immediate from Lemma~\ref{lemma:soundness19}.
% \end{proof}

% \end{document}
